<html>
<head><meta charset="utf-8"><title>weekly meeting 2019-01-21 · wg-traits · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/index.html">wg-traits</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html">weekly meeting 2019-01-21</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="156461743"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156461743" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156461743">(Jan 20 2019 at 02:19)</a>:</h4>
<p><span class="user-group-mention" data-user-group-id="692">@WG-compiler-traits</span>:</p>
<p>I just realized that this Monday is a holiday here in the US -- not sure if I can make the meeting or not. I could probably make it to the same time but on Tuesday. Should we consider rescheduling? </p>
<p>(<span class="user-mention" data-user-id="131694">@scalexm</span> was going to talk about how to handle trait objects in chalk)</p>



<a name="156473929"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156473929" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156473929">(Jan 20 2019 at 09:05)</a>:</h4>
<p>I think Tuesday same time is fine for me</p>



<a name="156483100"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156483100" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Sunjay Varma <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156483100">(Jan 20 2019 at 14:12)</a>:</h4>
<p>I won't be able to attend, but feel free to go on without me. My update is that I'm currently at a conference with Manish. Manish is leaving on Wednesday after which I will start work on specialization in chalk.</p>



<a name="156485302"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156485302" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156485302">(Jan 20 2019 at 15:23)</a>:</h4>
<p>That works for me</p>



<a name="156622724"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156622724" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156622724">(Jan 22 2019 at 17:33)</a>:</h4>
<p>So will we do the meeting today, <span class="user-group-mention" data-user-group-id="692">@WG-compiler-traits</span>? In ~90 minutes, I suppose.</p>



<a name="156629458"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156629458" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156629458">(Jan 22 2019 at 18:59)</a>:</h4>
<p>Any thoughts on how we should do this? :)</p>



<a name="156629486"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156629486" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156629486">(Jan 22 2019 at 18:59)</a>:</h4>
<p>I'm trying to pull together my thoughts from reading <a href="https://github.com/rust-lang-nursery/chalk/issues/203" target="_blank" title="https://github.com/rust-lang-nursery/chalk/issues/203">https://github.com/rust-lang-nursery/chalk/issues/203</a></p>



<a name="156629558"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156629558" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156629558">(Jan 22 2019 at 19:00)</a>:</h4>
<p>I'm not sure if we had planned to do a chat over video or just stick with Zulip</p>



<a name="156629575"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156629575" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156629575">(Jan 22 2019 at 19:00)</a>:</h4>
<p>I feel like we talked about it but I forget the answer :)</p>



<a name="156629757"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156629757" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156629757">(Jan 22 2019 at 19:02)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> just Zulip is a bit easier for me this evening, also I could do video</p>



<a name="156629764"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156629764" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156629764">(Jan 22 2019 at 19:02)</a>:</h4>
<p>ok that works for me</p>



<a name="156629765"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156629765" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156629765">(Jan 22 2019 at 19:02)</a>:</h4>
<p>I answered on the issue about the RFC you cited</p>



<a name="156629784"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156629784" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156629784">(Jan 22 2019 at 19:02)</a>:</h4>
<p>I see that, yes, I was thinking something similar</p>



<a name="156629823"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156629823" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156629823">(Jan 22 2019 at 19:03)</a>:</h4>
<p><span class="user-group-mention" data-user-group-id="692">@WG-compiler-traits</span> — guess we'll get started</p>



<a name="156629825"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156629825" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156629825">(Jan 22 2019 at 19:03)</a>:</h4>
<p>mmh no actually that wouldn't work because we also require <code>WellFormed(dyn  Foo) :- WellFormed(dyn Foo: Foo)</code></p>



<a name="156629901"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156629901" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156629901">(Jan 22 2019 at 19:04)</a>:</h4>
<p>and we somehow need this to prevent the possibility of naming types like <code>dyn Foo&lt;&amp;'a i32&gt;</code> where <code>trait Foo&lt;X&gt;: 'static</code></p>



<a name="156629910"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156629910" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156629910">(Jan 22 2019 at 19:04)</a>:</h4>
<p>something else to file for follow-up: we should discuss associatd item projection (e.g., <code>dyn Foo&lt;T = Bar&gt;</code>)</p>



<a name="156629945"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156629945" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156629945">(Jan 22 2019 at 19:04)</a>:</h4>
<p>so, the RFC, I was wondering if we want some in between</p>



<a name="156629975"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156629975" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156629975">(Jan 22 2019 at 19:05)</a>:</h4>
<p>i.e., if the trait is not object safe, maybe we permit the <code>dyn</code> type, but we don't add all the "implied bounds" rules</p>



<a name="156629998"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156629998" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156629998">(Jan 22 2019 at 19:05)</a>:</h4>
<p>er, I guess I mean the impls</p>



<a name="156630005"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156630005" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156630005">(Jan 22 2019 at 19:05)</a>:</h4>
<p>but I think we are getting ahead of ourselves</p>



<a name="156630092"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156630092" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156630092">(Jan 22 2019 at 19:06)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> I think <code>dyn Foo&lt;T = Bar&gt;</code> would just add some <code>Normalize</code> rules</p>



<a name="156630127"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156630127" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156630127">(Jan 22 2019 at 19:06)</a>:</h4>
<p>well basically in what I call the "generated impls", we would forward the specified associated type values</p>



<a name="156630160"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156630160" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156630160">(Jan 22 2019 at 19:07)</a>:</h4>
<p>the heart of your proposal is this rule, basically:</p>
<div class="codehilite"><pre><span></span>impl&lt;T1...Tk&gt; SuperTrait&lt;...&gt; for dyn Foo&lt;T1...Tk&gt; where SuperWC1[...], ..., SuperWCr[...]
{
}
</pre></div>



<a name="156630188"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156630188" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156630188">(Jan 22 2019 at 19:07)</a>:</h4>
<p>and I guess the WF rule:</p>
<div class="codehilite"><pre><span></span>WellFormed(dyn Foo&lt;X1...Xk&gt;) :-
    ObjectSafe(Foo),
    WellFormed(dyn Foo&lt;X1...Xk&gt;: Foo&lt;X1...Xk&gt;).
</pre></div>



<a name="156630196"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156630196" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156630196">(Jan 22 2019 at 19:07)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> right, but actually I believe the where clauses are not even needed (at least under an implied bounds setting), the real heart is the WF rule</p>



<a name="156630266"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156630266" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156630266">(Jan 22 2019 at 19:08)</a>:</h4>
<p>it's an interesting rule</p>



<a name="156630271"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156630271" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156630271">(Jan 22 2019 at 19:08)</a>:</h4>
<p>so you'll have to refresh my memory</p>



<a name="156630284"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156630284" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156630284">(Jan 22 2019 at 19:08)</a>:</h4>
<p>when we prove that <code>WF(T: Trait)</code>, does that assume that <code>WF(T)</code> is true?</p>



<a name="156630292"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156630292" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156630292">(Jan 22 2019 at 19:08)</a>:</h4>
<p>I know we talked about various different approaches to where to put the "recursion"</p>



<a name="156630301"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156630301" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156630301">(Jan 22 2019 at 19:08)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> yes kind of, basically <code>WF(T: Trait)</code> does not care at all about the well-formedness of types</p>



<a name="156630336"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156630336" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156630336">(Jan 22 2019 at 19:09)</a>:</h4>
<p>(meta-question: who else is around? Is it just <span class="user-mention" data-user-id="131694">@scalexm</span> and I?)</p>



<a name="156630353"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156630353" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156630353">(Jan 22 2019 at 19:09)</a>:</h4>
<p>/me is reading</p>



<a name="156630360"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156630360" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alexander Regueiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156630360">(Jan 22 2019 at 19:09)</a>:</h4>
<p>I'm around briefly</p>



<a name="156630419"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156630419" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156630419">(Jan 22 2019 at 19:10)</a>:</h4>
<p>me</p>



<a name="156630445"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156630445" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156630445">(Jan 22 2019 at 19:10)</a>:</h4>
<p>cool :)</p>



<a name="156630453"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156630453" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156630453">(Jan 22 2019 at 19:10)</a>:</h4>
<p>I am feeling a desire to briefly reiterate how the WF rules work again <span class="user-mention" data-user-id="131694">@scalexm</span> =)</p>



<a name="156630469"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156630469" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156630469">(Jan 22 2019 at 19:11)</a>:</h4>
<p>that's a very curious typing rule... which should never terminate unless <code>WF(T: Trait)</code> doesn't require <code>WF(T)</code>... right?</p>



<a name="156630495"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156630495" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156630495">(Jan 22 2019 at 19:11)</a>:</h4>
<p>correct, <span class="user-mention" data-user-id="126931">@centril</span>, that's partly why I was asking</p>



<a name="156630500"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156630500" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156630500">(Jan 22 2019 at 19:11)</a>:</h4>
<p><span class="user-mention" data-user-id="126931">@centril</span>  <code>WF(T: Trait)</code> does not assume anything</p>



<a name="156630511"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156630511" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156630511">(Jan 22 2019 at 19:11)</a>:</h4>
<p>and it does not try to prove any <code>WF(T)</code> either</p>



<a name="156630547"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156630547" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156630547">(Jan 22 2019 at 19:11)</a>:</h4>
<p>well-formedness for types comes from "outside", that is when the type checker see some type <code>Type</code> named somewhere, it will try to prove <code>WF(Type)</code></p>



<a name="156630593"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156630593" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alexander Regueiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156630593">(Jan 22 2019 at 19:12)</a>:</h4>
<p>what does well-formedness even mean?</p>



<a name="156630595"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156630595" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alexander Regueiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156630595">(Jan 22 2019 at 19:12)</a>:</h4>
<p>seems like a kind of vague term</p>



<a name="156630606"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156630606" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156630606">(Jan 22 2019 at 19:12)</a>:</h4>
<p><span class="user-mention" data-user-id="131694">@scalexm</span> is the rustc-guide up to date, do you now? (e.g., <a href="https://rust-lang.github.io/rustc-guide/traits/wf.html#trait-definitions" target="_blank" title="https://rust-lang.github.io/rustc-guide/traits/wf.html#trait-definitions">this section</a>)</p>



<a name="156630628"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156630628" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156630628">(Jan 22 2019 at 19:12)</a>:</h4>
<blockquote>
<p>what does well-formedness even mean?</p>
</blockquote>
<p>it means what we say it means :)</p>



<a name="156630642"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156630642" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156630642">(Jan 22 2019 at 19:12)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> the rustc-guide is up to date, except for the slight flaw I discovered</p>



<a name="156630653"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156630653" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156630653">(Jan 22 2019 at 19:12)</a>:</h4>
<p>yeah, ok</p>



<a name="156630692"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156630692" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156630692">(Jan 22 2019 at 19:13)</a>:</h4>
<p>(which btw I discovered by studying well-formedness for trait objects since you have some weird rule like <code>struct S&lt;T&gt; where S&lt;T&gt;: Trait</code>)</p>



<a name="156630710"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156630710" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156630710">(Jan 22 2019 at 19:13)</a>:</h4>
<p>except I linked to the wrong part</p>



<a name="156630759"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156630759" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156630759">(Jan 22 2019 at 19:14)</a>:</h4>
<p>the wf rules for traits are <a href="https://rust-lang.github.io/rustc-guide/traits/lowering-rules.html#implied-bounds" target="_blank" title="https://rust-lang.github.io/rustc-guide/traits/lowering-rules.html#implied-bounds">here, in the lowering section</a></p>



<a name="156630770"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156630770" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156630770">(Jan 22 2019 at 19:14)</a>:</h4>
<div class="codehilite"><pre><span></span>// Rule WellFormed-TraitRef
forall&lt;Self, P1..Pn&gt; {
  WellFormed(Self: Trait&lt;P1..Pn&gt;) :-
    Implemented(Self: Trait&lt;P1..Pn&gt;) &amp;&amp;
    WellFormed(WC)
}
</pre></div>



<a name="156630784"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156630784" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156630784">(Jan 22 2019 at 19:14)</a>:</h4>
<p>right</p>



<a name="156630826"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156630826" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156630826">(Jan 22 2019 at 19:15)</a>:</h4>
<p>so basically <span class="user-mention" data-user-id="124069">@Alexander Regueiro</span> saying that <code>T: Trait</code> is "well-formed" says that (a) it is implemented and (b) all the where clauses on the trait are satisfied</p>



<a name="156630844"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156630844" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156630844">(Jan 22 2019 at 19:15)</a>:</h4>
<p>(the prolog form of stating things feels so backwards stating the premises before the result... as compared to gentzen style...)</p>



<a name="156630855"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156630855" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alexander Regueiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156630855">(Jan 22 2019 at 19:15)</a>:</h4>
<p>okay. that means something totally different to logic hah. I thought it was some type-theoretical notion which had a correspondence to logic.</p>



<a name="156630857"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156630857" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156630857">(Jan 22 2019 at 19:15)</a>:</h4>
<p>ok, so to bring that back to the trait object rule:</p>
<div class="codehilite"><pre><span></span>WellFormed(dyn Foo&lt;X1...Xk&gt;) :-
    ObjectSafe(Foo),
    WellFormed(dyn Foo&lt;X1...Xk&gt;: Foo&lt;X1...Xk&gt;).
</pre></div>


<p>it certainly relies on the <code>Implemented</code> rule that we generate</p>



<a name="156630925"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156630925" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alexander Regueiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156630925">(Jan 22 2019 at 19:16)</a>:</h4>
<p>and what does "implemented" mean here?</p>



<a name="156630948"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156630948" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alexander Regueiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156630948">(Jan 22 2019 at 19:16)</a>:</h4>
<p>you mean the trait bound is satisfied?</p>



<a name="156630960"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156630960" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156630960">(Jan 22 2019 at 19:16)</a>:</h4>
<p>more or less. It means that we believe an impl exists (it may come from an in-scope where-clause, in some contexts)</p>



<a name="156630980"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156630980" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156630980">(Jan 22 2019 at 19:16)</a>:</h4>
<p>(or "witness" in type theory)</p>



<a name="156631015"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156631015" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156631015">(Jan 22 2019 at 19:17)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> yes: thanks to the <code>Implemented</code> rules we generate, only the where clauses that talk about lifetimes or type parameters may turn out to be false, all the other where clauses of the form <code>where Self: Trait&lt;...&gt;</code> are somehow "assumed" to be true because of the generated impls</p>



<a name="156631057"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156631057" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Taylor Cramer <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156631057">(Jan 22 2019 at 19:17)</a>:</h4>
<p>(perhaps it's worth mentioning trivial-where-clauses, where some of this breaks down)</p>



<a name="156631148"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156631148" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156631148">(Jan 22 2019 at 19:18)</a>:</h4>
<p>the impl rule we generate being as follows, I think?</p>
<div class="codehilite"><pre><span></span>forall&lt;T1..Tk&gt; {
  Implemented(dyn Foo&lt;T1..Tk&gt;: SuperTrait&lt;..&gt;) :-
    Implemented(SuperWC1[...]), ..., Implemented(SuperWCr[...])
}
</pre></div>


<p>ah, so, <span class="user-mention" data-user-id="131694">@scalexm</span>, to what extent are we relying on things being acyclic here..?</p>



<a name="156631153"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156631153" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Taylor Cramer <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156631153">(Jan 22 2019 at 19:18)</a>:</h4>
<p>since it allows assuming some things that aren't true globally-- but ignore me if I'm just distracting</p>



<a name="156631157"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156631157" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156631157">(Jan 22 2019 at 19:18)</a>:</h4>
<p><span class="user-mention" data-user-id="127859">@Taylor Cramer</span> I believe trivial-where-clauses are naturally handled in the new-style trait solving, basically we just always assume all where clauses to be true, we never check for "inconsistent" where clauses</p>



<a name="156631216"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156631216" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156631216">(Jan 22 2019 at 19:19)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> yes this is what we generate</p>



<a name="156631317"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156631317" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156631317">(Jan 22 2019 at 19:20)</a>:</h4>
<p>mmh I think cyclic traits are handled correctly, provided that we can get all the super-traits via some fixed point algorithm</p>



<a name="156631320"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156631320" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156631320">(Jan 22 2019 at 19:20)</a>:</h4>
<p>so e.g. if we have</p>
<div class="codehilite"><pre><span></span><span class="k">trait</span><span class="w"> </span><span class="n">Foo</span>: <span class="nc">Bar</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="p">}</span><span class="w"></span>
<span class="k">trait</span><span class="w"> </span><span class="n">Bar</span>: <span class="nc">Foo</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="p">}</span><span class="w"></span>
</pre></div>


<p>today, that's an error, but I'd like to remove that requirement.</p>



<a name="156631330"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156631330" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156631330">(Jan 22 2019 at 19:20)</a>:</h4>
<p>but as I noted this must be done outside of the logic</p>



<a name="156631355"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156631355" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156631355">(Jan 22 2019 at 19:20)</a>:</h4>
<p>I mean we must have some code in rustc that retrieves all the super-traits and generate the impls</p>



<a name="156631380"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156631380" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156631380">(Jan 22 2019 at 19:20)</a>:</h4>
<p>so let's walk through that example, maybe? just for my edification :)</p>



<a name="156631417"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156631417" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156631417">(Jan 22 2019 at 19:21)</a>:</h4>
<p>basically we would make two rules, lke so, right?</p>
<div class="codehilite"><pre><span></span>Implemented(dyn Foo: Foo) :- Implemented(dyn Foo: Bar).
Implemented(dyn Foo: Bar) :- Implemented(dyn Foo: Foo).
</pre></div>



<a name="156631488"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156631488" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156631488">(Jan 22 2019 at 19:22)</a>:</h4>
<p>er, I guess we would also have </p>
<div class="codehilite"><pre><span></span>Implemented(dyn Bar: Foo) :- Implemented(dyn Bar: Bar).
Implemented(dyn Bar: Bar) :- Implemented(dyn Bar: Foo).
</pre></div>


<p>coming from the <code>trait Bar</code> declaration</p>



<a name="156631492"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156631492" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156631492">(Jan 22 2019 at 19:22)</a>:</h4>
<p><span class="user-mention" data-user-id="131694">@scalexm</span> so if <code>WF(T: Trait) :- WF(T), ...</code> doesn't hold, then won't that make <code>[u8; "hello"]</code> legal and other such nonsense...? or do you check <code>WF(T)</code> later for <code>[u8; "hello"]</code> ?</p>



<a name="156631499"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156631499" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156631499">(Jan 22 2019 at 19:22)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> yeah ok it seems like it would not work with the where clauses on the generated impls</p>



<a name="156631517"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156631517" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156631517">(Jan 22 2019 at 19:22)</a>:</h4>
<p><em>however</em>, as I said, I think they are not necessary especially in the implied bounds setting</p>



<a name="156631525"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156631525" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156631525">(Jan 22 2019 at 19:22)</a>:</h4>
<p>ok, yeah, maybe we can drill into <em>that</em> a bit</p>



<a name="156631530"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156631530" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alexander Regueiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156631530">(Jan 22 2019 at 19:22)</a>:</h4>
<p>@centril cool. that's in terminology I'm familiar with</p>



<a name="156631531"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156631531" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156631531">(Jan 22 2019 at 19:22)</a>:</h4>
<p>basically I've written these where clauses at first so that these synthetic impls are well-formed (well-formedness of impls defined in the rustc-guide)</p>



<a name="156631557"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156631557" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156631557">(Jan 22 2019 at 19:23)</a>:</h4>
<p>(I kind of can't answer the question of what role they play exactly, I think)</p>



<a name="156631565"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156631565" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156631565">(Jan 22 2019 at 19:23)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> but with the reverse rules <code>FromEnv(dyn Foo: Foo) :- FromEnv(dyn Foo)</code> and since we do <code>impl Trait for dyn Foo</code>, we have <code>dyn Foo</code> in our env</p>



<a name="156631639"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156631639" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156631639">(Jan 22 2019 at 19:24)</a>:</h4>
<p>OK.</p>



<a name="156631656"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156631656" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156631656">(Jan 22 2019 at 19:24)</a>:</h4>
<p><span class="user-mention" data-user-id="126931">@centril</span> all types appearing in, say, a function are WF-checked in a separate pass indeed</p>



<a name="156631730"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156631730" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156631730">(Jan 22 2019 at 19:25)</a>:</h4>
<p>makes sense</p>



<a name="156631737"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156631737" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156631737">(Jan 22 2019 at 19:25)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> but basically the sentence I wrote on the issue:</p>
<blockquote>
<p>Note that, in the rules described earlier, we added where clauses from the super traits on every generated impl only so that the impl is well-formed even without implied bounds, I am not sure they are strictly needed.</p>
</blockquote>
<p>sums up the idea</p>



<a name="156631744"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156631744" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156631744">(Jan 22 2019 at 19:25)</a>:</h4>
<p>(ps, maybe we should find another name for <code>WellFormed(T: Trait)</code> -- even <code>WellFormedImpl</code> might be more obvious)</p>



<a name="156631810"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156631810" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156631810">(Jan 22 2019 at 19:26)</a>:</h4>
<p>(actually not sure that's more obvious ;)</p>



<a name="156631815"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156631815" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156631815">(Jan 22 2019 at 19:26)</a>:</h4>
<p>yeah bike-shedding is welcome :)</p>



<a name="156631842"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156631842" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alexander Regueiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156631842">(Jan 22 2019 at 19:26)</a>:</h4>
<p>can we come up with better terminology than well-formed, btw? it doesn't really give an intuitive idea of what it means... unless it's standard terminology, I guess. "witnessed" sounds good.</p>



<a name="156631856"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156631856" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alexander Regueiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156631856">(Jan 22 2019 at 19:26)</a>:</h4>
<p>oh</p>



<a name="156631857"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156631857" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alexander Regueiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156631857">(Jan 22 2019 at 19:26)</a>:</h4>
<p>heh</p>



<a name="156631859"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156631859" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alexander Regueiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156631859">(Jan 22 2019 at 19:26)</a>:</h4>
<p>just saw your message</p>



<a name="156631878"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156631878" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156631878">(Jan 22 2019 at 19:27)</a>:</h4>
<p><span class="user-mention" data-user-id="124069">@Alexander Regueiro</span> <code>WellFormed</code> for types has been a terminology floating around in the compiler for some time, and we just basically reused it for traits without thinking too much about it :p</p>



<a name="156631889"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156631889" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156631889">(Jan 22 2019 at 19:27)</a>:</h4>
<p>it's standard terminology</p>



<a name="156631893"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156631893" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156631893">(Jan 22 2019 at 19:27)</a>:</h4>
<p>(in particular, the goals of the "well-formedness checking" section are different from the "well formed" predicate)</p>



<a name="156631898"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156631898" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156631898">(Jan 22 2019 at 19:27)</a>:</h4>
<p>recent developments on implied bounds etc have basically been niko, <span class="user-mention" data-user-id="126804">@Ariel Ben-Yehuda</span> and myself</p>



<a name="156631948"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156631948" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156631948">(Jan 22 2019 at 19:28)</a>:</h4>
<p>maybe <code>FullyImplemented</code> or something...</p>



<a name="156631963"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156631963" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alexander Regueiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156631963">(Jan 22 2019 at 19:28)</a>:</h4>
<p>yeah. god knows how it became standard though. "well-formed" has syntactical connotations (both to the intuitive mind, and in formal logic)</p>



<a name="156631975"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156631975" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alexander Regueiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156631975">(Jan 22 2019 at 19:28)</a>:</h4>
<p>which is why I dislike it.</p>



<a name="156631988"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156631988" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alexander Regueiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156631988">(Jan 22 2019 at 19:28)</a>:</h4>
<p>FullyImplemented kind of works</p>



<a name="156631998"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156631998" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156631998">(Jan 22 2019 at 19:28)</a>:</h4>
<blockquote>
<p>(in particular, the goals of the "well-formedness checking" section are different from the "well formed" predicate)</p>
</blockquote>
<p>I remember this being confusing for sure</p>



<a name="156632011"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632011" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632011">(Jan 22 2019 at 19:28)</a>:</h4>
<p>the latter section might also be called "legality" or something</p>



<a name="156632016"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632016" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632016">(Jan 22 2019 at 19:28)</a>:</h4>
<p>i.e., it's the rules that make an impl <em>legal</em></p>



<a name="156632018"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632018" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632018">(Jan 22 2019 at 19:28)</a>:</h4>
<p>"legality" is good I think</p>



<a name="156632021"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632021" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632021">(Jan 22 2019 at 19:29)</a>:</h4>
<p>and other forms of declarations</p>



<a name="156632045"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632045" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632045">(Jan 22 2019 at 19:29)</a>:</h4>
<p>can we stick to standard terminology (especially that used by <em>Philip Wadler</em>)...? :P</p>



<a name="156632050"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632050" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alexander Regueiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632050">(Jan 22 2019 at 19:29)</a>:</h4>
<p>no, because it's shit? ;-)</p>



<a name="156632176"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632176" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632176">(Jan 22 2019 at 19:30)</a>:</h4>
<p>in gentzen style you might say:</p>
<div class="codehilite"><pre><span></span>Γ ⊢ σ type
Γ ⊢ x: usize
------------------
Γ ⊢ [σ; x] type
</pre></div>



<a name="156632189"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632189" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632189">(Jan 22 2019 at 19:30)</a>:</h4>
<p><span class="user-mention" data-user-id="126931">@centril</span> I'm not even sure we're really using <code>WellFormed(Type)</code> according to the standard terminology signification, do we?</p>



<a name="156632197"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632197" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alexander Regueiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632197">(Jan 22 2019 at 19:30)</a>:</h4>
<p>^^</p>



<a name="156632225"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632225" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632225">(Jan 22 2019 at 19:31)</a>:</h4>
<p><span class="user-mention" data-user-id="131694">@scalexm</span> not sure either... but I can read a wadler paper and... ;)</p>



<a name="156632230"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632230" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alexander Regueiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632230">(Jan 22 2019 at 19:31)</a>:</h4>
<p><span class="user-mention" data-user-id="126931">@centril</span> that's not what we're talking about here though I think</p>



<a name="156632241"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632241" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632241">(Jan 22 2019 at 19:31)</a>:</h4>
<p><code>σ type</code> meaning "σ is well-formed"</p>



<a name="156632242"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632242" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632242">(Jan 22 2019 at 19:31)</a>:</h4>
<p>basically WF rules are something like:</p>
<div class="codehilite"><pre><span></span><span class="k">struct</span> <span class="nc">S</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="w"> </span><span class="k">where</span><span class="w"> </span><span class="n">T</span>: <span class="nc">Debug</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="p">}</span><span class="w"></span>
</pre></div>


<div class="codehilite"><pre><span></span>WellFormed(S&lt;T&gt;) :- Implemented(T: Debug)
</pre></div>



<a name="156632265"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632265" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632265">(Jan 22 2019 at 19:31)</a>:</h4>
<p>so I don't even know if there is a connection to type theory or whatever (not my field of knowledge at all lol)</p>



<a name="156632316"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632316" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632316">(Jan 22 2019 at 19:32)</a>:</h4>
<p>I recommend reading <a href="https://homepages.inf.ed.ac.uk/wadler/papers/quantcc/quantcc.pdf" target="_blank" title="https://homepages.inf.ed.ac.uk/wadler/papers/quantcc/quantcc.pdf">https://homepages.inf.ed.ac.uk/wadler/papers/quantcc/quantcc.pdf</a></p>



<a name="156632323"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632323" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alexander Regueiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632323">(Jan 22 2019 at 19:32)</a>:</h4>
<p>I would say "the type S&lt;T&gt; has a witness"</p>



<a name="156632371"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632371" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alexander Regueiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632371">(Jan 22 2019 at 19:33)</a>:</h4>
<p>or "has a type instance", maybe better</p>



<a name="156632372"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632372" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632372">(Jan 22 2019 at 19:33)</a>:</h4>
<p>FWIW I find "legal" fairly intuitive</p>



<a name="156632403"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632403" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alexander Regueiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632403">(Jan 22 2019 at 19:33)</a>:</h4>
<p>"legal" doesn't work for me, because it looks legal at first sight, it just happens not to have an instance.</p>



<a name="156632407"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632407" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alexander Regueiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632407">(Jan 22 2019 at 19:33)</a>:</h4>
<p>i.e. it's empty</p>



<a name="156632411"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632411" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632411">(Jan 22 2019 at 19:33)</a>:</h4>
<p><span class="user-mention" data-user-id="116883">@tmandry</span> I think "legal" for type/trait/impl declarations is good indeed</p>



<a name="156632430"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632430" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632430">(Jan 22 2019 at 19:34)</a>:</h4>
<p><span class="user-mention" data-user-id="124069">@Alexander Regueiro</span> we're talking about declarations here, e.g. "is this <code>impl</code> block I wrote legal"</p>



<a name="156632472"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632472" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alexander Regueiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632472">(Jan 22 2019 at 19:34)</a>:</h4>
<p>so maybe <code>NonEmpty</code> works, unless I'm misunderstanding?</p>



<a name="156632480"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632480" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632480">(Jan 22 2019 at 19:34)</a>:</h4>
<p>legal is a synonym for well-formed... you haven't changed anything ;)</p>



<a name="156632485"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632485" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632485">(Jan 22 2019 at 19:34)</a>:</h4>
<p>I think <strong>legal</strong> is good for the goals that declare whether a declaration is accepted or whether an error is reported.</p>



<a name="156632503"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632503" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alexander Regueiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632503">(Jan 22 2019 at 19:34)</a>:</h4>
<p><span class="user-mention" data-user-id="131694">@scalexm</span> concrete example?</p>



<a name="156632509"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632509" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alexander Regueiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632509">(Jan 22 2019 at 19:34)</a>:</h4>
<p>that's not what I was talking about</p>



<a name="156632540"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632540" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632540">(Jan 22 2019 at 19:35)</a>:</h4>
<p><span class="user-mention" data-user-id="124069">@Alexander Regueiro</span> </p>
<div class="codehilite"><pre><span></span><span class="k">trait</span><span class="w"> </span><span class="n">Foo</span>: <span class="nb">Copy</span> <span class="p">{</span><span class="w"> </span><span class="p">}</span><span class="w"></span>

<span class="k">impl</span><span class="w"> </span><span class="n">Foo</span><span class="w"> </span><span class="k">for</span><span class="w"> </span><span class="nb">String</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="c1">// This impl is not legal</span>
<span class="p">}</span><span class="w"></span>
</pre></div>



<a name="156632550"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632550" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632550">(Jan 22 2019 at 19:35)</a>:</h4>
<p>today we say "this impl is not WF", which I agree is confusing :p</p>



<a name="156632559"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632559" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632559">(Jan 22 2019 at 19:35)</a>:</h4>
<p>because we already use <code>WellFormed</code> for so many things</p>



<a name="156632562"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632562" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alexander Regueiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632562">(Jan 22 2019 at 19:35)</a>:</h4>
<p>ohh that's something else entirely</p>



<a name="156632568"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632568" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alexander Regueiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632568">(Jan 22 2019 at 19:35)</a>:</h4>
<p>I think we're talking about two different things here</p>



<a name="156632570"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632570" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alexander Regueiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632570">(Jan 22 2019 at 19:35)</a>:</h4>
<p>and not just me</p>



<a name="156632577"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632577" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632577">(Jan 22 2019 at 19:35)</a>:</h4>
<p>yes, that's the point :)</p>



<a name="156632628"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632628" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alexander Regueiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632628">(Jan 22 2019 at 19:36)</a>:</h4>
<p>sorry guys</p>



<a name="156632636"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632636" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alexander Regueiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632636">(Jan 22 2019 at 19:36)</a>:</h4>
<p>I agree "legal" is good for that case :-)</p>



<a name="156632637"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632637" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alexander Regueiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632637">(Jan 22 2019 at 19:36)</a>:</h4>
<p>better than "well-formed"</p>



<a name="156632643"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632643" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632643">(Jan 22 2019 at 19:36)</a>:</h4>
<p>heh, not just you that is confused, never fear =)</p>



<a name="156632655"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632655" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632655">(Jan 22 2019 at 19:36)</a>:</h4>
<p><span class="user-mention" data-user-id="124069">@Alexander Regueiro</span> that's ok, at least we now see how confusing all these <code>WellFormed</code> everywhere are lol</p>



<a name="156632661"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632661" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alexander Regueiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632661">(Jan 22 2019 at 19:36)</a>:</h4>
<p>yep!</p>



<a name="156632675"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632675" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632675">(Jan 22 2019 at 19:36)</a>:</h4>
<p>so, to bring it back a bit to trait objects:</p>
<ul>
<li>we had these where-clauses on the impl because we wanted to ensure that it would meet the <strong>legality</strong> requirements (yay! new terminology)</li>
<li>but actually they follow from the implied bounds</li>
</ul>



<a name="156632694"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632694" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alexander Regueiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632694">(Jan 22 2019 at 19:37)</a>:</h4>
<p>so my vote is "witnessed" or "instantiated" for the first meaning, and "legal" for that meaning... but do we have a consensus already?</p>



<a name="156632707"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632707" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632707">(Jan 22 2019 at 19:37)</a>:</h4>
<p>I do not like either witnessed or instantiated :)</p>



<a name="156632727"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632727" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alexander Regueiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632727">(Jan 22 2019 at 19:37)</a>:</h4>
<p>okay</p>



<a name="156632728"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632728" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632728">(Jan 22 2019 at 19:37)</a>:</h4>
<p>but I'd rather we discuss that particular bikeshed later :)</p>



<a name="156632733"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632733" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632733">(Jan 22 2019 at 19:37)</a>:</h4>
<p>I also don't like well-formed, mind you :)</p>



<a name="156632737"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632737" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632737">(Jan 22 2019 at 19:37)</a>:</h4>
<blockquote>
<p>In addition to checking the well-formedness of the method type,we ensure that the class context(C1,...,Cn)is also well-formed,extending the environment with the local variablea. In turn, thisimplies thatfv(Ci)⊆ {a}, in line with the Haskell standard.</p>
<p>Type &amp; Constraint Well-ScopednessThe judgments for well-scopeness of types, constraints and axiom sets are denotedΓ⊢tyσ,Γ⊢ctCandΓ⊢axArespectively. Their definitions are straightforwardand can be found in Appendix A.</p>
<p>We check the well-formedness of the instance contextAun-der the extended typing environment, and that each superclassconstraintCiis entailed by the instance context.</p>
</blockquote>



<a name="156632742"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632742" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alexander Regueiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632742">(Jan 22 2019 at 19:37)</a>:</h4>
<p>fair. we'll leave that later</p>



<a name="156632746"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632746" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632746">(Jan 22 2019 at 19:37)</a>:</h4>
<p>so... well-formed is standard.</p>



<a name="156632755"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632755" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alexander Regueiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632755">(Jan 22 2019 at 19:37)</a>:</h4>
<p><span class="user-mention" data-user-id="126931">@centril</span> Wadler isn't the oracle though, you know. ;-)</p>



<a name="156632817"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632817" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632817">(Jan 22 2019 at 19:38)</a>:</h4>
<p>He is, he invented this stuff we are talking about... =P</p>



<a name="156632822"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632822" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alexander Regueiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632822">(Jan 22 2019 at 19:38)</a>:</h4>
<p>and standard doesn't mean good... though it does mean standard. anyway, we should weigh that against the fact most people who work on the compiler aren't type theorists</p>



<a name="156632831"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632831" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632831">(Jan 22 2019 at 19:38)</a>:</h4>
<p>(anyways...)</p>



<a name="156632848"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632848" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alexander Regueiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632848">(Jan 22 2019 at 19:38)</a>:</h4>
<p>I sincerely doubt it. This stuff has been around forever.</p>



<a name="156632874"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632874" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632874">(Jan 22 2019 at 19:38)</a>:</h4>
<p>ok, off topic :)</p>



<a name="156632879"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632879" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alexander Regueiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632879">(Jan 22 2019 at 19:38)</a>:</h4>
<p>yep</p>



<a name="156632913"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632913" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alexander Regueiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632913">(Jan 22 2019 at 19:39)</a>:</h4>
<p>back to Niko... next topic?</p>



<a name="156632919"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632919" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632919">(Jan 22 2019 at 19:39)</a>:</h4>
<p>so <span class="user-mention" data-user-id="131694">@scalexm</span> it seems like the "trait object implied bounds" is another key part</p>



<a name="156632933"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632933" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632933">(Jan 22 2019 at 19:39)</a>:</h4>
<p>I think the confusion arises from not being clear about what WF is with respect to... e.g. WF type, WF environment, WF super-trait constrants, ...</p>



<a name="156632957"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156632957" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156632957">(Jan 22 2019 at 19:39)</a>:</h4>
<p>but if I'm not mistaken, I don't see the <code>FromEnv</code> rules in your writeup... I must have missed them</p>



<a name="156633018"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156633018" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156633018">(Jan 22 2019 at 19:40)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> it's one very small paragraph I think</p>



<a name="156633061"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156633061" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156633061">(Jan 22 2019 at 19:40)</a>:</h4>
<p>oh, I see</p>



<a name="156633094"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156633094" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156633094">(Jan 22 2019 at 19:41)</a>:</h4>
<div class="codehilite"><pre><span></span>FromEnv(dyn Foo&lt;T1...Tk&gt;: Foo&lt;T1...Tk&gt;) :- FromEnv(dyn Foo&lt;T1...Tk&gt;)
</pre></div>



<a name="156633244"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156633244" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156633244">(Jan 22 2019 at 19:43)</a>:</h4>
<p>(btw if someone wants to know what <code>FromEnv</code> means and basically how implied bounds are supposed to work in the new style trait solver, I wrote a lot of things in the rustc guide, feedback on the understandability of what I wrote is welcome)</p>



<a name="156633329"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156633329" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156633329">(Jan 22 2019 at 19:44)</a>:</h4>
<p>I was just re-reading some of that indeed</p>



<a name="156633337"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156633337" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156633337">(Jan 22 2019 at 19:44)</a>:</h4>
<p>to bring it back in cache</p>



<a name="156633425"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156633425" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156633425">(Jan 22 2019 at 19:45)</a>:</h4>
<p>if I read that literally... then it says "if from the environment, we can assume dyn Foo&lt;T1...Tk&gt; is ????, we can prove that dyn Foo&lt;T1...Tk&gt;: Foo&lt;T1...Tk&gt; is ????"</p>



<a name="156633501"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156633501" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156633501">(Jan 22 2019 at 19:46)</a>:</h4>
<p>???? = legal?</p>



<a name="156633511"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156633511" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156633511">(Jan 22 2019 at 19:46)</a>:</h4>
<p><span class="user-mention" data-user-id="126931">@centril</span> seems like that yeah</p>



<a name="156633520"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156633520" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156633520">(Jan 22 2019 at 19:46)</a>:</h4>
<p>valid = WF ?</p>



<a name="156633531"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156633531" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156633531">(Jan 22 2019 at 19:46)</a>:</h4>
<p>oh gosh sorry</p>



<a name="156633545"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156633545" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156633545">(Jan 22 2019 at 19:47)</a>:</h4>
<p>I meant "legal"</p>



<a name="156633644"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156633644" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156633644">(Jan 22 2019 at 19:48)</a>:</h4>
<p>to summarize, I guess:</p>
<ul>
<li><code>WellFormed(Ty)</code> -- indicates that a type is "valid", meaning that all the where clauses etc on the type are met.</li>
<li><code>WellFormed(T0: Trait&lt;T1..Tn&gt;)</code> -- indicates that a trait-ref is valid, meaning that it and all of its transitive where clauses are implemented. I'll call this <em>fully implemented</em> for now to distinguish it.</li>
</ul>
<p>Applied to this particular case, we are saying that <code>dyn Foo</code> has sort of implied "where clauses":</p>
<ul>
<li>the trait must be object safe</li>
<li>the trait reference <code>dyn Foo: Foo</code> must be "fully implemented"</li>
</ul>



<a name="156633685"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156633685" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156633685">(Jan 22 2019 at 19:49)</a>:</h4>
<p>actually, when we do WF checking in chalk (where we produce and check WF goals), is that meaning of WF also covered by "legal"?</p>



<a name="156633770"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156633770" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156633770">(Jan 22 2019 at 19:50)</a>:</h4>
<p><span class="user-mention" data-user-id="116883">@tmandry</span> in chalk, <code>src/rules/wf.rs</code> is where we check if trait/type/impl declarations are legal</p>



<a name="156633785"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156633785" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156633785">(Jan 22 2019 at 19:51)</a>:</h4>
<p>I am thinking about a few things:</p>
<ul>
<li>We should discuss a bit what happens with <code>dyn Foo + Bar</code></li>
<li>Earlier, I was mentioning that it might be nice to think of extending instead with a true existential type and talking about how we would deal with that in a more "first-class" way. I want to try and map that back and forth a bit between these rules still</li>
</ul>



<a name="156633799"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156633799" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156633799">(Jan 22 2019 at 19:51)</a>:</h4>
<p><span class="user-mention" data-user-id="116883">@tmandry</span>  and proving that something is legal ends up generating <code>WellFormed(...)</code> goals :)</p>



<a name="156633909"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156633909" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156633909">(Jan 22 2019 at 19:52)</a>:</h4>
<p><span class="user-mention" data-user-id="131694">@scalexm</span> ok. so to clarify, have we decided to rename the <code>WellFormed(...)</code> goal, or not?</p>



<a name="156633920"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156633920" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156633920">(Jan 22 2019 at 19:52)</a>:</h4>
<p><span class="user-mention" data-user-id="116883">@tmandry</span> not yet</p>



<a name="156633949"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156633949" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156633949">(Jan 22 2019 at 19:53)</a>:</h4>
<p><span class="user-mention" data-user-id="116883">@tmandry</span> but we may decide to rename to "legality checking" the process that is happening in e.g. <code>src/rules/wf.rs</code> in chalk</p>



<a name="156633967"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156633967" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156633967">(Jan 22 2019 at 19:53)</a>:</h4>
<p>okay, thanks, makes sense now.</p>



<a name="156633981"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156633981" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156633981">(Jan 22 2019 at 19:53)</a>:</h4>
<blockquote>
<p>ok. so to clarify, have we decided to rename the <code>WellFormed(...)</code> goal, or not?</p>
</blockquote>
<p>I think we have decided to rename it, but not what to rename it <em>to</em></p>



<a name="156634033"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156634033" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156634033">(Jan 22 2019 at 19:54)</a>:</h4>
<p>also, there are really two distinct goals (<code>WellFormed(Ty)</code> and <code>WellFormed(TraitReference)</code>) and likely they should not have the same name</p>



<a name="156634039"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156634039" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156634039">(Jan 22 2019 at 19:54)</a>:</h4>
<p>I'd write <code>WFType(...)</code>, <code>WFConstraint(...)</code>, <code>WFOtherThing(...)</code></p>



<a name="156634056"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156634056" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156634056">(Jan 22 2019 at 19:54)</a>:</h4>
<p>to make it clear what sort of well-formedness we're talking about</p>



<a name="156634069"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156634069" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156634069">(Jan 22 2019 at 19:54)</a>:</h4>
<p>(sure)</p>



<a name="156634082"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156634082" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156634082">(Jan 22 2019 at 19:55)</a>:</h4>
<p>we can spin-off a new channel for bike-shedding</p>



<a name="156634093"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156634093" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156634093">(Jan 22 2019 at 19:55)</a>:</h4>
<p>I'm feeling a desire <span class="user-mention" data-user-id="131694">@scalexm</span> to try and draw up a kind of diagram for implied bounds</p>



<a name="156634105"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156634105" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156634105">(Jan 22 2019 at 19:55)</a>:</h4>
<p>(and object types, to some extent)</p>



<a name="156634113"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156634113" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156634113">(Jan 22 2019 at 19:55)</a>:</h4>
<p>trying to show "this thing can be assumed to be true" because "so and so proves it here"</p>



<a name="156634209"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156634209" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156634209">(Jan 22 2019 at 19:56)</a>:</h4>
<p>anyway, I probably gotta go, but this was definitely helpful. Re: naming, a separate topic sounds like a good idea</p>



<a name="156634233"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156634233" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156634233">(Jan 22 2019 at 19:57)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> I see</p>



<a name="156634271"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156634271" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156634271">(Jan 22 2019 at 19:57)</a>:</h4>
<p>that may help indeed, although I'm not sure what said diagram would look like</p>



<a name="156634360"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156634360" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156634360">(Jan 22 2019 at 19:58)</a>:</h4>
<p>me either :)</p>



<a name="156634363"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156634363" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156634363">(Jan 22 2019 at 19:59)</a>:</h4>
<p>it may prove hard to do</p>



<a name="156634380"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156634380" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156634380">(Jan 22 2019 at 19:59)</a>:</h4>
<p>I spun out the <a href="#narrow/stream/144729-wg-traits/topic/bikeshedding.20.22well.20formed.22" title="#narrow/stream/144729-wg-traits/topic/bikeshedding.20.22well.20formed.22">"bikeshedding well formed"</a> topic btw</p>



<a name="156634518"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156634518" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156634518">(Jan 22 2019 at 20:01)</a>:</h4>
<p><span class="user-mention" data-user-id="131694">@scalexm</span> just to check, the <a href="https://rust-lang.github.io/rustc-guide/traits/lowering-rules.html#lowering-type-definitions" target="_blank" title="https://rust-lang.github.io/rustc-guide/traits/lowering-rules.html#lowering-type-definitions">writeup in the rustc guide</a> suggests that when lowering a struct declaration like</p>
<div class="codehilite"><pre><span></span><span class="k">struct</span> <span class="nc">Foo</span><span class="o">&lt;</span><span class="n">T</span>: <span class="nb">Eq</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="p">...</span><span class="w"> </span><span class="p">}</span><span class="w"></span>
</pre></div>


<p>we would make a rule:</p>
<div class="codehilite"><pre><span></span><span class="n">forall</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">  </span><span class="n">WellFormed</span><span class="p">(</span><span class="n">Foo</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="p">)</span><span class="w"> </span>:<span class="o">-</span><span class="w"> </span><span class="n">Implemented</span><span class="p">(</span><span class="n">T</span>: <span class="nb">Eq</span><span class="p">)</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>
</pre></div>


<p>but actually it's a <em>tad</em> unclear to me, because we write <code>WellFormed(Type&lt;P1..Pn&gt;) :- WC</code> (I guess that here when we "paste in" WC we map to <code>Implemented</code>, right?)</p>



<a name="156634546"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156634546" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156634546">(Jan 22 2019 at 20:01)</a>:</h4>
<p>(in particular I was wondering if we needed the stronger <code>WellFormed(T: Eq)</code>)</p>



<a name="156634631"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156634631" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156634631">(Jan 22 2019 at 20:02)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> we need it</p>



<a name="156634649"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156634649" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156634649">(Jan 22 2019 at 20:02)</a>:</h4>
<p>Because of the flaw indeed</p>



<a name="156634652"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156634652" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156634652">(Jan 22 2019 at 20:02)</a>:</h4>
<p>yes ok I see</p>



<a name="156634705"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156634705" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156634705">(Jan 22 2019 at 20:03)</a>:</h4>
<p>well that is mildly gratifying, in that my "intuition" was that we likely wanted it, but I can't honestly say why :)</p>



<a name="156634779"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156634779" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156634779">(Jan 22 2019 at 20:04)</a>:</h4>
<p>It was just an « optimization » at first, but turns out it was wrong</p>



<a name="156635008"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/weekly%20meeting%202019-01-21/near/156635008" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/weekly.20meeting.202019-01-21.html#156635008">(Jan 22 2019 at 20:07)</a>:</h4>
<p>Thanks <span class="user-mention" data-user-id="131694">@scalexm</span> for the writeup btw =) <span class="emoji emoji-2764" title="heart">:heart:</span></p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>